Aspects of Incompleteness: Chapter 2, Incompleteness
$ \mathbf{Q} \vdash G \leftrightarrow \lnot \mathrm{Pr}_T(\ulcorner G \urcorner)
となる$ \Pi_1文$ Gが存在する.$ GはGödel文 このとき$ T \nvdash Gである.
更に$ Gが真で,$ Tが$ \Sigma_1健全なら$ T \nvdash \lnot G
proof
$ T \vdash Gと仮定する.
$ Gの定義より$ \mathbf{Q} \vdash \lnot Gで,よって$ T \vdash \lnot G.
今$ Tは無矛盾と仮定したからおかしい.よって$ T \nvdash G.
もし$ Gが真だとすると$ \lnot Gは偽の$ \Sigma_1文である.
$ Tは$ \Sigma_1健全($ Tで証明可能→真)だから対偶(偽→$ Tで証明不能)より$ T \nvdash \lnot G